$\forall$${\it da}$:$k$:Knd fp$\rightarrow$ Type, $k$:Knd. Msgtype(${\it da}$;$k$) $\in$ Type